theory ClangEv imports Main BehBase ClangSem
begin

--"event in a global trace"
--"(index in global trace, process name, process execution step)"
datatype ('pn,'n,'m,'l) gevent 
  = Gevent nat 'pn "('pn,'n,'m,'l) pstep"

fun ge_n :: "('pn,'n,'m,'l) gevent \<Rightarrow> nat"
  where "ge_n (Gevent j _ _) = j"
fun ge_proc :: "('pn,'n,'m,'l) gevent \<Rightarrow> 'pn"
  where "ge_proc (Gevent _ p _) = p"
fun ge_stp :: "('pn,'n,'m,'l) gevent \<Rightarrow> ('pn,'n,'m,'l) pstep"
  where "ge_stp (Gevent _ _ stp) = stp"

--"events form a linear preorder"
instantiation gevent :: (type,type,type,type) linpreorder
begin
definition "x \<prec> y = (ge_n x < ge_n y)"
definition "x \<preceq> y = (ge_n x \<le> ge_n y)"
definition "x \<parallel> y = (ge_n x = ge_n y)"
instance proof
qed (auto simp add: less_gevent_def less_eq_gevent_def par_gevent_def)
end

--"is an event in a process execution step"
fun estepev :: 
     "('pn,'n,'m,'l) estate \<Rightarrow> ('pn,'n,'m,'l) estate \<Rightarrow> ('pn,'n,'m,'l) pstep \<Rightarrow> bool"
where
  "estepev (Estate s1 q1 io1 True) (Estate s2 q2 _ _) pst = 
                                                (pst = (Pstep s1 q1 io1 s2 q2))"
| "estepev (Estate _ _ _ False) _ _ = False"

--"is an event in a given global trace"
fun globev :: "('pn,'n,'m,'l) gtrace \<Rightarrow> ('pn,'n,'m,'l) gevent \<Rightarrow> bool"
where
  "globev tr (Gevent j p stp) = 
     ( gst_ests (tr j) p \<noteq> None 
      \<and> gst_ests (tr (Suc j)) p \<noteq> None
      \<and> (estepev (the (gst_ests (tr j) p)) (the (gst_ests (tr (Suc j)) p)) stp))"

fun read_ge :: "'m \<Rightarrow> ('pn,'n,'m,'l) gevent \<Rightarrow> bool" --"is a read event"
where
  "read_ge svar e = 
     (io_read (pstep_io (ge_stp e)) \<and> var_io (pstep_io (ge_stp e)) = Some svar)"

fun writeto_ge :: "'m \<Rightarrow> ('pn,'n,'m,'l) gevent \<Rightarrow> bool" --"is a write event"
where
  "writeto_ge svar e = 
     (io_write (pstep_io (ge_stp e)) \<and> var_io (pstep_io (ge_stp e)) = Some svar)"

fun ge_val :: "('pn,'n,'m,'l) gevent ~=> vals" --"value of an IO action of event"
where
  "ge_val e = val_io (pstep_io (ge_stp e))"

(*-----------------------------------------------------------------------------*)

lemma valid_gtrans_expr: "valid_gtrans g1 g2 = 
            (globtrans (gst_ests g1) (gst_sh g1) (gst_ests g2) (gst_sh g2))"
by (cases g1, cases g2, auto)

lemma read_ge_rep:
  "read_ge (x::'m) e \<and> ge_val e = Some w \<Longrightarrow> pstep_io (ge_stp e) = ARead x w"
proof (cases e, auto)
  fix stp
  assume "io_read (pstep_io stp)" "var_io (pstep_io stp) = Some x" "val_io (pstep_io stp) = Some w"
  then show "pstep_io stp = ARead x w"
  proof (cases stp, auto)
    fix io
    assume "io_read io" "var_io io = Some x" "val_io io = Some w"
    then show "io = ARead x w" by (cases io, auto)
  qed
qed

lemma read_ge_val: "read_ge (x::'m) e \<Longrightarrow> \<exists> w . ge_val e = Some w"
proof (cases e, auto)
  fix stp
  assume "io_read (pstep_io stp)" "var_io (pstep_io stp) = Some x"
  then show "\<exists> w . val_io (pstep_io stp) = Some w"
  proof (cases stp, auto)
    fix io
    assume "io_read io" "var_io io = Some x"
    then show "\<exists> w. val_io io = Some w" by (cases io, auto)
  qed
qed

lemma writeto_ge_rep: 
  "writeto_ge (x::'m) e \<and> ge_val e = Some w \<Longrightarrow> pstep_io (ge_stp e) = AWrite x w"
proof (cases e, auto)
  fix stp
  assume "io_write (pstep_io stp)" "var_io (pstep_io stp) = Some x" "val_io (pstep_io stp) = Some w"
  then show "pstep_io stp = AWrite x w"
  proof (cases stp, auto)
    fix io
    assume "io_write io" "var_io io = Some x" "val_io io = Some w"
    then show "io = AWrite x w" by (cases io, auto)
  qed
qed

lemma writeto_ge_val: "writeto_ge (x::'m) e \<Longrightarrow> \<exists> w . ge_val e = Some w"
proof (cases e, auto)
  fix stp
  assume "io_write (pstep_io stp)" "var_io (pstep_io stp) = Some x"
  then show "\<exists> w . val_io (pstep_io stp) = Some w"
  proof (cases stp, auto)
    fix io
    assume "io_write io" "var_io io = Some x"
    then show "\<exists> w. val_io io = Some w" by (cases io, auto)
  qed
qed

fun tres_ev:: "('pn,'n,'m,'l) gtrace \<Rightarrow> ('pn,'n,'m,'l) gevent ~=> ('pn,'n,'m,'l) estate"
where
  "tres_ev tr e = (gst_ests (tr (ge_n e))) (ge_proc e)"

fun trsh_ev:: "('pn,'n,'m,'l) gtrace \<Rightarrow> ('pn,'n,'m,'l) gevent \<Rightarrow> ('m ~=> vals)"
where
  "trsh_ev tr e = (gst_sh (tr (ge_n e)))"

fun es_of_ev:: "('pn,'n,'m,'l) gevent \<Rightarrow> ('pn,'n,'m,'l) estate"
where
  "es_of_ev e = ( Estate (pstep_curstm (ge_stp e)) 
                         (pstep_cur (ge_stp e))
                         (pstep_io (ge_stp e))
                          True )"

fun ev_stm :: "('pn,'n,'m,'l) gevent \<Rightarrow> ('pn,'n,'m,'l) stmt"
  where "ev_stm e = es_stm (es_of_ev e)"

lemma esevent:
  fixes tr e
  assumes a1:"valid_gtrace tr" "globev tr e"
  shows "tres_ev tr e = Some (es_of_ev e)"
proof -
  obtain n where y1:"n = (ge_n e)" by blast
  obtain p where y2:"p = (ge_proc e)" by blast
  from a1 y1 y2 obtain stp where c0:"e = Gevent n p stp" by (metis ge_n.simps ge_proc.simps gevent.exhaust)
  from this a1(2) have c1:"gst_ests (tr n) p \<noteq> None" "gst_ests (tr (Suc n)) p \<noteq> None" "estepev (the (gst_ests (tr n) p)) (the (gst_ests (tr (Suc n)) p)) stp" by auto
  then obtain es where c2:"gst_ests (tr n) p = Some es" by auto
  from c1 obtain es' where c3:"gst_ests (tr (Suc n)) p = Some es'" by auto
  obtain s q io s' q' where c4:"stp = (Pstep s q io s' q')" by (metis pstep.exhaust)

  from c1 c2 c3 have d1:"estepev es es' stp" by auto
  obtain s1 q1 io1 b1 where d2:"es = (Estate s1 q1 io1 b1)" by (metis estate.exhaust)
  obtain s2 q2 io2 b2 where d3:"es' = (Estate s2 q2 io2 b2)" by (metis estate.exhaust)
  from d1 d2 d3 have "b1 = True \<and> stp = (Pstep s1 q1 io1 s2 q2)" by (cases b1, auto)

  from this c4 d2 have "es = (Estate s q io True)" by auto
  from this c2 c4 c0 y1 y2 show ?thesis by (metis es_of_ev.simps ge_stp.simps pstep_cur.simps pstep_curstm.simps pstep_io.simps tres_ev.simps) 
qed

lemma lem_io_helper:
  fixes tr e
  assumes a1:"valid_gtrace tr" "globev tr e"
  shows "eo_io (tres_ev tr e) = pstep_io (ge_stp e)"
proof -
  have "eo_io (Some (es_of_ev e)) = pstep_io (ge_stp e)" by simp
  from this a1 show ?thesis using esevent by metis
qed

lemma read_ge_sh:
  fixes tr x e w
  assumes a0: "valid_gtrace tr" "globev tr e"
  assumes a1: "read_ge x e \<and> ge_val e = Some w"
  shows "trsh_ev tr e x = Some w"
proof -
  obtain n where c1:"n = (ge_n e)" by blast
  obtain p where c2:"p = (ge_proc e)" by blast
  let ?pes = "gst_ests (tr n)"
  let ?sh = "gst_sh (tr n)"
  have "eo_io (?pes p) = ARead x w"
  proof -
    from a1 have "pstep_io (ge_stp e) = ARead x w" using read_ge_rep by simp
    from this a0 have "eo_io (tres_ev tr e) = ARead x w" using lem_io_helper by metis
    from this c1 c2 show ?thesis by simp
  qed
  then have "(ARead x w) \<in> all_ios ?pes" by (simp, metis)
  moreover have "chk_reads (all_ios ?pes) ?sh"
  proof -
    from a0 have "valid_gtrans (tr n) (tr (Suc n))" using valid_gtrace_def by blast
    then show ?thesis using globtrans_def valid_gtrans_expr by blast
  qed
  ultimately have "?sh x = Some w" by simp
  from this c1 show ?thesis by simp
qed

lemma gev_equiv:
  assumes a0:"valid_gtrace tr" "globev tr e1" "globev tr e2"
  and a1: "ge_n e1 = ge_n e2" "ge_proc e1 = ge_proc e2"
  shows "e1 = e2"
proof -
  from a1 obtain n where y1:"n = (ge_n e1) \<and> n = (ge_n e2)" by blast
  from a1 obtain p where y2:"p = (ge_proc e1) \<and> p = (ge_proc e2)" by blast
  from y1 y2 obtain stp1 stp2 where c0:"e1 = Gevent n p stp1 \<and> e2 = Gevent n p stp2" by (metis ge_n.simps ge_proc.simps gevent.exhaust)

  from this a0(2) have c1:"gst_ests (tr n) p \<noteq> None" "gst_ests (tr (Suc n)) p \<noteq> None"
    "estepev (the (gst_ests (tr n) p)) (the (gst_ests (tr (Suc n)) p)) stp1" by auto
  from c0 a0(3) have c2: "estepev (the (gst_ests (tr n) p)) (the (gst_ests (tr (Suc n)) p)) stp2" by auto

  from c1 obtain es where c3:"gst_ests (tr n) p = Some es" by auto
  from c1 obtain es' where c4:"gst_ests (tr (Suc n)) p = Some es'" by auto

  from c1 c2 c3 c4 have d0:"estepev es es' stp1" "estepev es es' stp2" by auto
  obtain s1 q1 io1 b1 where d1:"es = (Estate s1 q1 io1 b1)" by (metis estate.exhaust)
  obtain s2 q2 io2 b2 where d2:"es' = (Estate s2 q2 io2 b2)" by (metis estate.exhaust)
  from d0 d1 d2 have "stp1 = stp2" by (cases b1, auto)
  from this c0 show ?thesis by simp
qed

lemma lem_share:
  fixes tr e1 e2
  assumes a0:"valid_gtrace tr" "globev tr e1" "globev tr e2"
  and a1: "(read_ge x e1 \<or> writeto_ge x e1) \<and> (read_ge x e2 \<or> writeto_ge x e2)"
  shows "e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1"
proof -
  {
    assume "e1 \<parallel> e2"
    then obtain n where c1:"n = ge_n e1 \<and> n = ge_n e2" 
         using par_gevent_def by blast
    let ?pes = "gst_ests (tr n)"
    let ?p1 = "ge_proc e1"
    let ?p2 = "ge_proc e2"
    let ?es1 = "?pes ?p1"
    let ?es2 = "?pes ?p2"
    from a0 have "valid_gtrans (tr n) (tr (Suc n))" using valid_gtrace_def by blast
    then have "compat_ios ?pes" using globtrans_def valid_gtrans_expr by blast
    then have c2:"?p1 = ?p2 \<or> io_compat (eo_io ?es1) (eo_io ?es2)" by auto
    obtain io1 where d1:"io1 = pstep_io (ge_stp e1)" by auto
    obtain io2 where d2:"io2 = pstep_io (ge_stp e2)" by auto
    from a0 c1 d1 d2 have z0:"eo_io ?es1 = io1 \<and> eo_io ?es2 = io2" using lem_io_helper by auto
    from this c2 have z1:"?p1 = ?p2 \<or> io_compat io1 io2" by simp
    from a1 d1 obtain w1 where z2:"io1 = ARead x w1 \<or> io1 = AWrite x w1" using read_ge_rep read_ge_val writeto_ge_rep writeto_ge_val by metis
    from a1 d2 obtain w2 where z3:"io2 = ARead x w2 \<or> io2 = AWrite x w2" using read_ge_rep read_ge_val writeto_ge_rep writeto_ge_val by metis
    from z1 z2 z3 have "?p1 = ?p2" by auto
    from this c1 a0 have "e1 = e2" using gev_equiv by blast
  }
  then show ?thesis 
          using axpar by (metis less_le_not_le linpreorder_class.linear)
qed

lemma wri_helper1:
  fixes tr n x
  assumes a0:"valid_gtrace tr"
  and a1:"\<not> (\<exists> p w. eo_io ((gst_ests (tr n)) p) = AWrite x w)"
  shows "gst_sh (tr n) x = gst_sh (tr (Suc n)) x"
proof -
  from a0 have c1:"valid_gtrans (tr n) (tr (Suc n))" using valid_gtrace_def by blast
  obtain pes sh pes' sh' where c2:"(tr n) = (Gstate pes sh) \<and> (tr (Suc n)) = (Gstate pes' sh')" by (metis gstate.exhaust)
  from c1 c2 have "chk_writes (all_ios pes) sh sh'" by (simp only: valid_gtrans.simps globtrans_def)
  moreover have "\<not> (\<exists> w. AWrite x w \<in> (all_ios pes))"
  proof
    assume "\<exists> w. AWrite x w \<in> (all_ios pes)"
    then obtain w where "AWrite x w \<in> (all_ios pes)" by blast
    then obtain p where "eo_io (pes p) = AWrite x w" by auto
    from this a1 c2 show "False" by simp
  qed
  ultimately have "sh x = sh' x" by (simp only: chk_writes.simps, metis)
  from this c2 show ?thesis by simp
qed

lemma wri_helper2:
  fixes tr n x p w
  assumes a0:"valid_gtrace tr"
  and a1:"eo_io ((gst_ests (tr n)) p) = AWrite x w"
  shows "gst_sh (tr (Suc n)) x = Some w"
proof -
  from a0 have c1:"valid_gtrans (tr n) (tr (Suc n))" using valid_gtrace_def by blast
  obtain pes sh pes' sh' where c2:"(tr n) = (Gstate pes sh) \<and> (tr (Suc n)) = (Gstate pes' sh')" by (metis gstate.exhaust)
  from c1 c2 have "chk_writes (all_ios pes) sh sh'" by (simp only: valid_gtrans.simps globtrans_def)
  moreover have c3:"AWrite x w \<in> (all_ios pes)"
  proof -
    from a1 c2 have "eo_io (pes p) = AWrite x w" by auto
    then show ?thesis by (simp, metis)
  qed
  ultimately have "\<exists> k . AWrite x k \<in> (all_ios pes) \<and> sh' x = Some k" by auto
  then obtain k where c4:"AWrite x k \<in> (all_ios pes) \<and> sh' x = Some k" by blast
  from c1 c2 have c5:"compat_ios pes" by (simp only: valid_gtrans.simps globtrans_def)
  from c3 c5 obtain p where d1:"AWrite x w = eo_io (pes p)" by auto
  from c3 c4 obtain p' where d2:"AWrite x k = eo_io (pes p')" by auto
  from c5 d1 d2 have "p = p' \<or> io_compat (AWrite x w) (AWrite x k)" by auto
  from this d1 d2 have "k = w" by (metis io_compat.simps(6) the.simps val_io.simps(3))
  from this c4 have "sh' x = Some w" by simp
  from this c2 show ?thesis by simp
qed

lemma prog_init_sh: "prog_semantics prog tr \<Longrightarrow> gst_sh (tr 0) = empty"
  by (cases "tr 0", auto simp add: prog_semantics_def)

lemma natmax_helper: "\<exists> a . P a \<and> (\<forall> x . (P (x::nat) \<longrightarrow> x \<le> y)) \<Longrightarrow> \<exists> y0 . P y0 \<and> (\<forall> x . (P x \<longrightarrow> x \<le> y0))"
  apply(induct y, auto)
  by (metis le_Suc_eq)

lemma natmax_helper2: "\<exists> a . a \<in> A \<and> (\<forall> x . ((x::nat) \<in> A \<longrightarrow> x \<le> y)) \<Longrightarrow> \<exists> y0 . y0 \<in> A \<and> (\<forall> x . (x \<in> A \<longrightarrow> x \<le> y0))"
  using natmax_helper by (metis mem_def)

lemma lem_rw:
  fixes tr x e
  assumes ninit: "gst_sh (tr 0) = empty"
  assumes a0: "valid_gtrace tr" "globev tr e"
  assumes a1: "read_ge x e \<and> ge_val e = Some w"
  shows "\<exists> e' . e'\<prec>e 
               \<and> globev tr e' 
               \<and> writeto_ge x e' 
               \<and> ge_val e' = Some w 
               \<and> (\<forall> e''. e''\<preceq>e \<and> globev tr e'' \<and> writeto_ge x e'' \<longrightarrow> e'' \<preceq> e')"
proof -
  obtain n where c1:"n = ge_n e" by blast
  from a0 a1 have "trsh_ev tr e x = Some w" using read_ge_sh by simp
  from this c1 have c2:"gst_sh (tr n) x = Some w" by simp
  obtain inds where c3:"inds = { i . i<n \<and> (\<exists> p w' . eo_io ((gst_ests (tr i)) p) = AWrite x w') }" by blast
  have "inds \<noteq> {}"
  proof -
    {
      assume "\<forall> i<n . \<not> (\<exists> p w'. eo_io ((gst_ests (tr i)) p) = AWrite x w')"
      from this a0 have "\<forall> i<n . (gst_sh (tr i) x = gst_sh (tr (Suc i)) x)" using wri_helper1 by metis
      then have "gst_sh (tr 0) x = gst_sh (tr n) x" by (induct n, auto)
      from this ninit c2 have "False" by simp
    }
    from this c3 show ?thesis by blast
  qed
  then obtain j where "inds j" by (metis all_not_in_conv mem_def)
  moreover have "\<forall> i . (inds i \<longrightarrow> i \<le> n)"
  proof clarify
    fix i
    assume "inds i"
    then have "i \<in> inds" by (metis mem_def)
    from this c3 show "i \<le> n" using mem_def by auto
  qed
  ultimately obtain k where z1:"inds k \<and> (\<forall> i . (inds i \<longrightarrow> i \<le> k))" using natmax_helper by blast
  then have "k \<in> inds" by (metis mem_def)
  from this c3 have zle1:"k<n \<and> (\<exists> p w . eo_io ((gst_ests (tr k)) p) = AWrite x w)" by blast
  then obtain p w' where z2:"eo_io ((gst_ests (tr k)) p) = AWrite x w'" by blast
  obtain es1 where d1:"gst_ests (tr k) p = es1" by blast
  obtain es2 where d2:"gst_ests (tr (Suc k)) p = es2" by blast

  from z2 d1 have r0:"eo_io es1 = AWrite x w'" by simp
  then have "\<exists> s1 q1 io1 . es1 = Some (Estate s1 q1 io1 True)"
  proof (cases es1, simp)
    fix a
    assume "eo_io es1 = AWrite x w'" "es1 = Some a"
    then show "\<exists>s1 q1 io1. es1 = Some (Estate s1 q1 io1 True)"
      apply(cases a, auto)
      by (metis Collect_def empty_Collect_eq empty_def eo_io.simps(2) ioact.simps(5))
  qed
  then obtain s1 q1 io1 where r1:"es1 = Some (Estate s1 q1 io1 True)" by blast
  from a0 have "valid_gtrans (tr k) (tr (Suc k))" using valid_gtrace_def by blast
  from this d1 d2 have "etrans es1 es2" by (cases "tr k", cases "tr (Suc k)", auto simp add: globtrans_def)
  from this r1 have "\<exists> s2 q2 io2 b2 . es2 = Some (Estate s2 q2 io2 b2)" by (cases es2, simp, case_tac "a", simp) (*for constructive etrans*)
  then obtain s2 q2 io2 b2 where r2:"es2 = Some (Estate s2 q2 io2 b2)" by blast
  obtain stp where r3:"stp = (Pstep s1 q1 io1 s2 q2)" by blast
  obtain e' where r4:"e' = Gevent k p stp" by blast
  have "e' \<prec> e"
  proof -
    from zle1 c1 r4 have "ge_n e' < ge_n e" by simp
    then show ?thesis using less_gevent_def by auto
  qed
  moreover from d1 r1 d2 r2 r3 r4 have "globev tr e'" by auto
  moreover from r0 r1 r3 r4 have "writeto_ge x e'" by auto
  moreover have "ge_val e' = Some w"
  proof -
    from r4 r3 r1 r0 have t1:"ge_val e' = Some w'" by auto
    from z2 a0 have t2:"gst_sh (tr (Suc k)) x = Some w'" using wri_helper2 by metis
    have "\<forall> i<n . \<not> (i < Suc k) \<longrightarrow> (gst_sh (tr i) x = gst_sh (tr (Suc i)) x)"
    proof auto
      fix i
      assume l1:"i<n" "\<not> i < Suc k"
      have "\<not> (\<exists> p1 w1. eo_io ((gst_ests (tr i)) p1) = AWrite x w1)"
      proof
        assume "\<exists> p1 w1. eo_io ((gst_ests (tr i)) p1) = AWrite x w1"
        from l1 this c3 have "i \<in> inds" by auto
        from this z1 l1 show "False" by (metis le_imp_less_Suc mem_def)
      qed
      from this a0 show "gst_sh (tr i) x = gst_sh (tr (Suc i)) x" using wri_helper1 by metis
    qed
    then have "n \<le> Suc k \<or> gst_sh (tr (Suc k)) x = gst_sh (tr n) x"
      apply(induct n, auto)
      by (metis le_SucE lessI less_not_refl)
    from this zle1 have "n = Suc k \<or> gst_sh (tr (Suc k)) x = gst_sh (tr n) x" by auto
    from this t2 c2 t1 show ?thesis by auto
  qed
  moreover have "\<forall> e''. e''\<preceq>e \<and> globev tr e'' \<and> writeto_ge x e'' \<longrightarrow> e'' \<preceq> e'"
  proof clarify
    fix e''
    assume o1:"e'' \<preceq> e" "globev tr e''" "writeto_ge x e''"
    obtain n'' p'' where o2:"n'' = ge_n e''" "p'' = ge_proc e''" by blast
    from a0 o1 o2 have "eo_io ((gst_ests (tr n'')) p'') = pstep_io (ge_stp e'')" using lem_io_helper by auto
    moreover from o1 obtain w'' where o3:"pstep_io (ge_stp e'') = AWrite x w''" using writeto_ge_val writeto_ge_rep by metis
    ultimately have o4:"eo_io ((gst_ests (tr n'')) p'') = AWrite x w''" by simp
    moreover {
      assume "e'' \<prec> e"
      from this o2 c1 have "n'' < n" using less_gevent_def by blast
      from this o4 c3 have "n'' \<in> inds" by blast
      from this z1 have "n''\<le>k" by (metis mem_def)
      moreover from o2 r4 have "ge_n e'' = n'' \<and> ge_n e' = k" by auto
      ultimately have "e'' \<preceq> e'" using less_eq_gevent_def by blast
    }
    moreover {
      assume "e'' \<parallel> e \<and> e'' \<noteq> e"
      moreover from a0 a1 o1 have "e'' = e \<or> e'' \<prec> e \<or> e \<prec> e''" using lem_share by metis
      ultimately have "False" by (metis axpar less_le_not_le o1(1))
    }
    ultimately show "e'' \<preceq> e'" using axpar a1 o1 o3
      by (metis io_read.simps(3) less_le_not_le read_ge.simps)
  qed
  ultimately show ?thesis by metis
qed

lemma lem_lin:
  assumes a0:"valid_gtrace tr \<and> globev tr e1 \<and> globev tr e2"
  and a1:"ge_proc e1 = ge_proc e2"
  shows "e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1"
using a0 a1 axpar gev_equiv par_gevent_def 
by (metis less_le_not_le linpreorder_class.linear)

(*------------------------------------------------------------------*)

fun is_proc_ev where "is_proc_ev p e = (ge_proc e = p)"

interpretation langevents: Events_base
  "prog_semantics" --"trace"
  "globev"         --"ev"
  "is_proc_ev"     --"proc"
  "read_ge"        --"read"
  "writeto_ge"     --"writeto"
  "ge_val"         --"val"
proof
  --"axcompl"
  fix pg tr e
  assume "prog_semantics pg tr \<and> globev tr e"
  then show "\<exists> p. is_proc_ev p e" by simp
next
  --"axlin"
  fix pg tr e1 e2
  assume c1:"prog_semantics pg tr \<and> globev tr e1 \<and> globev tr e2"
  assume "\<exists> p. is_proc_ev p e1 \<and> is_proc_ev p e2"
  then have "ge_proc e1 = ge_proc e2" by auto
  from this c1 show "e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1" using lem_lin prog_semantics_def by blast
next
  --"axshare"
  fix pg tr e1 e2 x
  assume "prog_semantics pg tr \<and> globev tr e1 \<and> globev tr e2"
  moreover assume "(read_ge x e1 \<or> writeto_ge x e1) \<and> (read_ge x e2 \<or> writeto_ge x e2)"
  ultimately show "e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1" using lem_share prog_semantics_def by metis
next
  --"axrw"
  fix pg tr e x w
  assume "prog_semantics pg tr \<and> globev tr e"
  moreover assume "read_ge x e \<and> ge_val e = Some w"
  ultimately show "\<exists>e'. globev tr e' \<and> e' \<prec> e \<and> writeto_ge x e' \<and> ge_val e' = Some w \<and> (\<forall>e''. globev tr e'' \<and> e'' \<preceq> e \<and> writeto_ge x e'' \<longrightarrow> e'' \<preceq> e')"
  using lem_rw prog_init_sh prog_semantics_def by metis
next
  --"axexclio"
  fix pg tr e x y
  assume "prog_semantics pg tr \<and> globev tr e"
  moreover assume "read_ge x e \<and> writeto_ge y e"
  ultimately show "False" by (simp, cases "pstep_io(ge_stp e)", auto)
qed

(*---------------------------------------------------------------------------------------------------------*)

--"process execution sequence"
fun exseq :: "('pn,'n,'m,'l) gtrace \<Rightarrow> 'pn \<Rightarrow> nat ~=> ('pn,'n,'m,'l) estate"
where
  "exseq tr p i = (gst_ests (tr i) p)"

lemma ev_in_exseq:
  fixes tr e p
  assumes a0:"valid_gtrace tr" "globev tr e" "ge_proc e = p"
  shows "exseq tr p (ge_n e) = Some (es_of_ev e)"
using a0 esevent by auto

lemma exseq_trans:
  fixes tr p i
  assumes a0:"valid_gtrace tr"
  shows "etrans (exseq tr p i) (exseq tr p (Suc i))"
proof -
  from a0 have c1:"valid_gtrans (tr i) (tr (Suc i))" by (simp add: valid_gtrace_def)
  then show ?thesis by (metis Suc_eq_plus1 exseq.simps globtrans_def valid_gtrans_expr)
qed

lemma exseq_pre:
  fixes tr p n
  assumes a0:"valid_gtrace tr" "exseq tr p n \<noteq> None"
  shows "\<forall> i \<le> n . exseq tr p i \<noteq> None"
proof -
  obtain f where b1:"f = (\<lambda> i j. etrans (exseq tr p i) (exseq tr p j))" by blast
  obtain g where b2:"g = (\<lambda> i . (exseq tr p i) \<noteq> None)" by blast
  from a0 b1 have c1:"\<forall> i . (f i (Suc i))" using exseq_trans by metis
  have "\<forall> i . etrans (exseq tr p i) (exseq tr p (Suc i)) \<and> (exseq tr p (Suc i)) \<noteq> None \<longrightarrow> (exseq tr p i) \<noteq> None"
    by (metis etrans.simps(3))
  from this b1 b2 have c2:"\<forall> i . (f i (Suc i)) \<and> g (Suc i) \<longrightarrow> g i" by blast
  from c1 c2 have c3:"\<forall> i . g (Suc i) \<longrightarrow> g i" by blast
  from b2 a0 have c4:"g n" by blast
  from c3 c4 have "\<forall> i \<le> n . g i"
    apply(induct n)
    apply(simp)
    by (metis le_SucE)
  from this b2 show ?thesis by simp
qed

lemma exseq_pre2:
  assumes a0:"valid_gtrace tr" "globev tr e" "i \<le> ge_n e"
  shows "exseq tr (ge_proc e) i \<noteq> None"
proof -
  from a0 have "exseq tr (ge_proc e) (ge_n e) = Some (es_of_ev e)" using ev_in_exseq by metis
  then have "exseq tr (ge_proc e) (ge_n e) \<noteq> None" by auto
  from this a0 show ?thesis using exseq_pre by metis
qed

lemma exseq_pre3: "valid_gtrace tr \<Longrightarrow> exseq tr p (Suc i) = Some es \<Longrightarrow> \<exists> es' . exseq tr p i = Some es'"
  using exseq_trans by (metis etrans.simps(3) not_None_eq option.simps(2))

lemma exseq_to_ev:
  fixes tr p i stp
  assumes a0:"valid_gtrace tr" "exseq tr p (Suc i) \<noteq> None"
  and a1:"estepev (the (exseq tr p i)) (the (exseq tr p (Suc i))) stp"
  shows "globev tr (Gevent i p stp)"
proof -
  from a0 have "exseq tr p i \<noteq> None" using exseq_trans by (metis etrans.simps(3))
  from this a0 a1 show ?thesis by simp
qed

lemma exseq_to_ev2:
  fixes tr p i e stp
  assumes a0:"valid_gtrace tr" "globev tr e"
  and a1:"i \<le> ge_n e" "p = ge_proc e"
  and a2:"estepev (the (exseq tr p i)) (the (exseq tr p (Suc i))) stp"
  shows "globev tr (Gevent i p stp)"
proof -
  from a1 have "i = ge_n e \<or> (Suc i) \<le> ge_n e" by auto
  moreover {
    assume "i = ge_n e"
    from this a1 obtain stp' where "e = (Gevent i p stp')" by (metis ge_n.simps ge_proc.simps gevent.exhaust)
    from this a0 have "gst_ests (tr i) p \<noteq> None \<and> gst_ests (tr (Suc i)) p \<noteq> None" by simp
    from this a2 have ?thesis by simp
  }
  moreover {
    assume "Suc i \<le> ge_n e"
    from a0 a1 this have "exseq tr p (Suc i) \<noteq> None" using exseq_pre2 by auto
    from this a0 a1 a2 have ?thesis using exseq_to_ev by metis
  }
  ultimately show ?thesis by blast
qed

lemma exseq_init:
  assumes a0: "prog_semantics pg tr"
  and a1:"globev tr e" "proc \<in> set pg" "proc_name proc = ge_proc e"
  shows "\<exists> io bv . exseq tr (ge_proc e) 0 = Some (Estate (proc_stm proc) empty io bv)"
proof -
  from a1 obtain p where b0:"p = proc_name proc \<and> p = ge_proc e" by simp
  from a0 have c0:"valid_gtrace tr" using prog_semantics_def by blast
  from a1 this have "exseq tr (ge_proc e) 0 \<noteq> None" using exseq_pre2 by blast
  then obtain es where c1:"exseq tr (ge_proc e) 0 = Some es" by (metis not_None_eq)
  obtain stm q io bv where c2:"es = (Estate stm q io bv)" by (cases es, blast)
  from a0 have c3:"is_prog_init pg (tr 0)" using prog_semantics_def by blast
  then obtain pes0 sh0 where c4:"(tr 0) = (Gstate pes0 sh0)" by (cases "tr 0", auto)
  from a1 b0 c3 c4 have c5:"is_proc_inito proc (pes0 p)" by auto
  from b0 c1 c4 have "pes0 p = Some es" by auto
  from this c5 c2 have "stm = proc_stm proc \<and> q = empty" by (cases proc, simp)
  from this c2 c1 show ?thesis by blast
qed

lemma lem_ev_validstp: "valid_gtrace tr \<Longrightarrow> globev tr e \<Longrightarrow> valid_pstep (ge_stp e)"
apply(cases e, simp_all)
apply(case_tac "gst_ests (tr nat) pn", simp_all)
apply(case_tac "gst_ests (tr (Suc nat)) pn", simp_all)
apply(case_tac "a")
apply(case_tac "aa")
apply(case_tac "bool", simp_all)
apply(case_tac "tr nat", simp_all)
apply(case_tac "tr (Suc nat)", simp_all)
apply(clarify)
apply(subgoal_tac "etrans (fun1 pn) (fun1a pn)")
defer
apply(simp add: valid_gtrace_def)
apply(subgoal_tac "valid_gtrans (tr nat) (tr (Suc nat))")
defer
apply(blast)
defer
apply(simp only: valid_gtrans.simps globtrans_def)
apply(subgoal_tac "etrans (fun1 pn) (fun1a pn)")
defer
apply(blast)
defer
apply(simp)
apply(simp)
done

(*---------------------------IO events-------------------------------------------------------------------*)

fun rdetwc :: "'m \<Rightarrow> ('n,'m) wcond \<Rightarrow> bool"
where
  "rdetwc x (Weq x' _) = (x' = x)"
| "rdetwc x (Wneq x' _) = (x' = x)"

fun rdetect :: "'m \<Rightarrow> ('pn,'n,'m,'l) stmt \<Rightarrow> bool"
where
  "rdetect x (Cseq _ s _) = rdetect x s"
| "rdetect x (Cread _ _ x') = (x' = x)"
| "rdetect x (Cwait _ wcs _) = (\<exists> wc \<in> set wcs . rdetwc x wc)"
| "rdetect _ _ = False"

fun wdetect :: "'m \<Rightarrow> ('pn,'n,'m,'l) stmt \<Rightarrow> bool"
where
  "wdetect x (Cseq _ s _) = wdetect x s"
| "wdetect x (Cwrite _ x' _) = (x' = x)"
| "wdetect _ _ = False"

fun vdetect :: "('pn,'n,'m,'l) stmt ~=> vals"
where
  "vdetect (Cseq _ s _) = vdetect s"
| "vdetect (Cwrite _ _ (Eimm a)) = Some a"
| "vdetect _ = None"

(*------------------------------------------------------------*)

fun val_compat_expr::"vals \<Rightarrow> 'n expr \<Rightarrow> bool"
where
  "val_compat_expr a (Eimm a') = (a = a')"
| "val_compat_expr a _ = True"

fun val_compat_nexpr::"vals \<Rightarrow> 'n expr \<Rightarrow> bool"
where
  "val_compat_nexpr a (Eimm a') = (a \<noteq> a')"
| "val_compat_nexpr a _ = True"

fun r_compat_wc::"'m \<Rightarrow> vals \<Rightarrow> ('n,'m) wcond \<Rightarrow> bool"
where
  "r_compat_wc x a (Weq x' expr) = (x' = x \<and> val_compat_expr a expr)"
| "r_compat_wc x a (Wneq x' expr) = (x' = x \<and> val_compat_nexpr a expr)"

--"(ARead x a) action is compatible with a disjunction of wait conditions"
definition r_compat_wcs::"'m \<Rightarrow> vals \<Rightarrow> ('n,'m) wconds \<Rightarrow> bool"
where
  "r_compat_wcs x a wcs = (\<exists> wc \<in> set wcs . r_compat_wc x a wc)"

fun wcsdetect::"('pn,'n,'m,'l) stmt ~=> ('n,'m) wconds"
where
  "wcsdetect (Cseq _ s _) = wcsdetect s"
| "wcsdetect (Cwait _ wcs _) = (Some wcs)"
| "wcsdetect _ = None"

lemma lem_wcsdet:
  fixes tr e x a 
  assumes a0: "valid_gtrace tr" "globev tr e" "read_ge x e" "ge_val e = Some a"
  and a1: "wcsdetect (ev_stm e) = Some wcs"
  shows "r_compat_wcs x a wcs"
proof -
  have z1:"\<And> q wcs. check_wcs wcs q (ARead x a) \<longrightarrow> r_compat_wcs x a wcs"
    apply(auto simp add: r_compat_wcs_def)
    apply(subgoal_tac "r_compat_wc x a wc")
    apply(blast)
    apply(case_tac "wc", auto)
    apply(case_tac "expr", auto)
    apply(case_tac "expr", auto)
    done

  have z2:"\<And> s1 q1 . \<forall> s2 q2 . transition s1 q1 (ARead x a) s2 q2 \<and> wcsdetect s1 = (Some wcs) \<longrightarrow> r_compat_wcs x a wcs"
    apply(induct_tac s1)
    apply(simp)
    defer
    apply(case_tac "expr", simp, simp add: transition.simps)
    apply(simp, simp, simp, simp)

    apply(simp only: wcsdetect.simps transition.simps)
    apply(clarify)
    apply(metis z1)

    apply(simp only: transit_seq)
    apply(metis ioact.simps(3) wcsdetect.simps(1))
    done

  have z3: "valid_pstep (ge_stp e) \<Longrightarrow> read_ge x e \<Longrightarrow> ge_val e = Some a \<Longrightarrow> wcsdetect (ev_stm e) = Some wcs \<Longrightarrow> r_compat_wcs x a wcs"
    apply(cases e)
    apply(case_tac "pstep")
    apply(case_tac "ioact")
    apply(auto)
    apply(metis z2)
    done

  show ?thesis using a0 a1 lem_ev_validstp z3 by metis
qed

lemma lem_rdet:
  assumes a0: "valid_gtrace tr" "globev tr e"
  shows "(read_ge x e \<longrightarrow> rdetect x (ev_stm e)) \<and> (rdetect x (ev_stm e) \<longrightarrow> (\<exists> y . read_ge y e))"
proof -
  have lem_rdet_he0: "\<And> lb wcs s q1 x w s2 q2. transition (Cwait lb wcs s) q1 (ARead x w) s2 q2 \<longrightarrow> rdetect x (Cwait lb wcs s)"
    apply(auto)
    apply(subgoal_tac "rdetwc x wc", auto)
    apply(case_tac "wc", auto)
    done

  have lem_rdet_he1: "\<And> s1 q1 x w. \<forall> s2 q2 . transition s1 q1 (ARead x w) s2 q2 \<longrightarrow> rdetect x s1"
    apply(induct_tac s1)
    apply(simp)
    defer
    apply(case_tac "expr", simp) apply(metis ioact.simps transition.simps)
    apply(clarify) apply(metis ioact.simps transition.simps)
    apply(clarsimp)
    apply(clarsimp)
    apply(clarsimp) apply(case_tac "eval_expr q1 expr", simp, simp)
    apply(clarify) apply(metis lem_rdet_he0)
    apply(auto simp only: transit_seq) apply(auto)
    done

  have lem_rdet_he2: "\<And> s1 q1 io x . \<forall> s2 q2 . (transition s1 q1 io s2 q2 \<and> rdetect x s1 \<longrightarrow> io_read io \<and> (\<exists> y. var_io io = Some y))"
    apply(induct_tac s1)
    apply(simp)
    defer
    apply(simp, simp, simp)
    apply(case_tac "io")
    apply(simp, simp, simp, simp)
    apply(clarify)
    apply(case_tac "io", simp, simp, simp)
    apply(clarify)
    apply(simp only: transit_seq)
    apply(metis rdetect.simps)
    done
  have lem_rdet_he3: "valid_pstep (ge_stp e) \<Longrightarrow> read_ge x e \<Longrightarrow> rdetect x (ev_stm e)"
    apply(cases e)
    apply(case_tac "pstep")
    apply(case_tac "ioact")
    apply(auto simp add: lem_rdet_he1)
    done
  have lem_rdet_he4: "valid_pstep (ge_stp e) \<Longrightarrow> rdetect x (ev_stm e) \<Longrightarrow> \<exists> y . read_ge y e"
    apply(cases e)
    apply(case_tac "pstep", simp)
    by (metis lem_rdet_he2)
  show ?thesis using a0 lem_rdet_he3 lem_rdet_he4 lem_ev_validstp by metis
qed

lemma lem_wdet:
  assumes a0: "valid_gtrace tr" "globev tr e"
  shows "writeto_ge x e = wdetect x (ev_stm e)"
proof -
  have lem_wdet_he1: "\<And> s1 q1 x w. \<forall> s2 q2 . transition s1 q1 (AWrite x w) s2 q2 \<longrightarrow> wdetect x s1"
    apply(induct_tac s1)
    apply(simp)
    defer
    apply(case_tac "expr", simp) apply(metis ioact.simps(6) transition.simps(3))
    apply(clarify) apply(metis ioact.simps(5) transition.simps(5))
    apply(clarify) apply(metis ioact.simps(5) transition.simps(6))
    apply(clarsimp)
    apply(clarsimp) apply(case_tac "eval_expr q1 expr", simp, simp)
    apply(clarsimp)
    apply(auto simp only: transit_seq) apply(auto)
    done
  have lem_wdet_he2: "\<And> s1 q1 io x . \<forall> s2 q2 . transition s1 q1 io s2 q2 \<and> wdetect x s1 \<longrightarrow> io_write io \<and> var_io io = Some x"
    apply(induct_tac s1)
    apply(simp)
    defer
    apply(simp, simp, simp, simp, simp)
    apply(case_tac "eval_expr q1 expr")
    apply(simp, simp, simp)
    apply(clarify)
    apply(simp only: transit_seq)
    apply(metis wdetect.simps(1) wdetect.simps(3))
    done
  have lem_wdet_he3: "valid_pstep (ge_stp e) \<Longrightarrow> writeto_ge x e \<Longrightarrow> wdetect x (ev_stm e)"
    apply(cases e)
    apply(case_tac "pstep")
    apply(case_tac "ioact")
    apply(auto simp add: lem_wdet_he1)
    done
  have lem_wdet_he4: "valid_pstep (ge_stp e) \<Longrightarrow> wdetect x (ev_stm e) \<Longrightarrow> writeto_ge x e"
    apply(cases e)
    apply(case_tac "pstep", simp)
    by (metis lem_wdet_he2)
  show ?thesis using a0 lem_wdet_he3 lem_wdet_he4 lem_ev_validstp by metis
qed

lemma lem_vdet:
  assumes a0:"valid_gtrace tr" "globev tr e" "vdetect (ev_stm e) = Some w"
  shows "ge_val e = Some w"
proof -
  have lem_vdet_he1: "\<And> s1 q1 io w . \<forall> s2 q2 . transition s1 q1 io s2 q2 \<and> vdetect s1 = Some w \<longrightarrow> val_io io = Some w"
    apply(induct_tac s1)
    apply(simp)
    defer
    apply(simp, simp, simp, simp)
    apply(case_tac "eval_expr q1 expr", simp, simp)
    apply(case_tac "expr", simp, simp)
    apply(simp)
    apply(clarify)
    apply(simp only: transit_seq)
    by (metis option.simps(3) vdetect.simps(1) vdetect.simps(3))
  have lem_vdet_he2: "valid_pstep (ge_stp e) \<Longrightarrow> vdetect (ev_stm e) = Some w \<Longrightarrow> ge_val e = Some w"
    apply(cases e)
    apply(case_tac "pstep", simp)
    by (metis lem_vdet_he1)
  show ?thesis using a0 lem_vdet_he2 lem_ev_validstp by metis
qed


end
